|
| creator |
Bouajjani, Ahmed
| | Esparza, Javier
| | Schwoon, Stefan
| | Strejcek, Jan
| | date |
2005-11-29
| | | | description |
18 pages
| |
We introduce asynchronous dynamic pushdown networks (ADPN), a new
model for multithreaded programs in which pushdown systems
communicate via shared memory. ADPN generalizes both CPS (concurrent
pushdown systems) and DPN (dynamic pushdown networks). We show that
ADPN exhibit several advantages as a program model. Since the
reachability problem for ADPN is undecidable even in the case
without dynamic creation of processes, we address the bounded
reachability problem, which considers only those computation
sequences where the (index of the) thread accessing the shared
memory is changed at most a fixed given number of times. We provide
efficient algorithms for both forward and backward reachability
analysis. The algorithms are based on automata techniques for
symbolic representation of sets of configurations.
| | format |
application/pdf
| | 187549 Bytes | |